c formula generated with seed 6, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.408889
c the planted solution is {1, 3, 5, 6, 10, 11, 13, 14, 15, 18, 19, 20, 21, 22, 23, 24, 27, 28, 29, 31, 32, 34, 35, 39, 40, 46, 49, 63, 68, 69, 70, 72, 73, 74, 76, 79, 80, 81, 83, 84, 86, 87, 89, 94, 95, 96, 98, 99, 100, 101, 102, 105, 106, 107, 109, 110, 114, 115, 119, 121, 123, 125, 126, 129, 131, 135, 136, 139, 147, 149, 151, 153, 155, 157, 161, 162, 166, 167, 170, 172, 175, 176, 177, 179, 180, 181, 182, 183, 186, 188, 190, 195, 196, 197, 199, 201, 202, 205, 209, 212, 213, 218, 221, 222, 226, 227, 228, 231, 236, 237, 242, 247, 249, 252, 255, 257, 260, 261, 262, 263, 265, 266, 276, 278, 279, 280, 281, 283, 284, 285, 290, 291, 292, 294, 296, 298, 300, 302, 304, 306, 308, 309, 310, 315, 316, 317, 318, 321, 322, 327, 329, 331, 332, 335, 336, 337, 338, 339, 341, 345, 347, 348, 352, 353, 355, 357, 360, 362, 363, 369, 370, 373, 374, 375, 376, 377, 378, 379, 380, 383, 384, 385, 391, 392, 393, 394, 397, 400, 405, 406, 409, 410, 411, 412, 413, 414, 415, 416, 418, 422, 424, 425, 429, 430, 434, 435, 436, 438, 439, 440, 441, 442, 445, 446, 449}
p cnf 450 1984
-19 391 -65 0
52 -111 -135 0
226 107 105 0
-217 -249 293 0
13 -158 -248 0
354 377 -400 0
283 -258 -395 0
5 233 388 0
-141 -408 -122 0
-179 392 433 0
3 -29 187 0
26 40 399 0
38 -331 -417 0
322 -129 171 0
-53 86 -448 0
-158 416 -371 0
449 375 422 0
298 46 -38 0
200 302 -236 0
28 -291 402 0
329 -118 -344 0
-167 394 -249 0
-308 -129 -387 0
-25 304 -116 0
139 449 -381 0
-36 300 166 0
-279 -247 -328 0
-68 139 -336 0
443 -234 444 0
-64 129 -82 0
-345 434 127 0
371 62 -104 0
17 11 344 0
-297 400 414 0
14 87 -258 0
-294 -97 103 0
349 -418 -244 0
-53 -274 -331 0
-387 -66 376 0
433 414 -165 0
-41 -384 169 0
263 -237 -279 0
340 136 193 0
-442 60 218 0
-299 310 -173 0
-12 -126 320 0
135 180 374 0
-210 -203 -117 0
-380 -411 213 0
49 -429 -306 0
-36 -383 -1 0
122 -290 345 0
327 -26 -75 0
286 -31 -256 0
-354 -57 -444 0
-354 -436 -276 0
210 -443 -27 0
-221 258 -361 0
-190 266 -418 0
-411 -292 -158 0
-419 110 332 0
128 -316 -320 0
-69 435 73 0
-403 -19 -227 0
-427 182 -343 0
-246 3 1 0
-193 -73 208 0
13 -415 365 0
134 15 364 0
-252 -182 80 0
328 -200 7 0
-212 273 129 0
-300 87 -86 0
419 -32 410 0
-98 105 165 0
-269 -449 -170 0
-116 -161 -209 0
353 339 82 0
-330 -65 72 0
69 -241 18 0
275 36 218 0
55 -250 272 0
226 438 322 0
190 91 -337 0
325 450 -208 0
-71 130 -416 0
-125 -303 -98 0
-64 -420 -411 0
-303 -272 -152 0
185 310 408 0
-334 -218 -221 0
312 -241 -380 0
39 3 -268 0
-16 -186 -430 0
-236 -187 143 0
74 -237 -31 0
156 -439 29 0
-133 -4 -361 0
-184 -24 3 0
282 -417 -348 0
-140 419 -436 0
114 137 184 0
-140 -360 -304 0
-406 -300 360 0
-188 -358 389 0
114 153 292 0
155 -26 438 0
45 -418 -163 0
185 117 -158 0
372 158 -77 0
-414 87 372 0
160 -107 249 0
80 342 85 0
310 -42 -254 0
-273 443 111 0
-267 124 142 0
-143 -192 -450 0
-353 384 356 0
-268 -208 -69 0
-281 120 409 0
208 335 -18 0
-374 212 -386 0
210 -44 -372 0
111 -91 277 0
297 314 300 0
372 428 -47 0
251 -324 -380 0
246 161 -222 0
137 -192 207 0
321 -437 183 0
440 -187 -134 0
-253 -113 -191 0
183 -74 -335 0
126 -8 414 0
412 -418 312 0
342 -268 223 0
-401 -237 -430 0
-304 305 -346 0
-287 354 -291 0
249 -53 170 0
56 -430 177 0
-9 -443 -57 0
55 -420 64 0
-148 147 -48 0
-389 144 313 0
-68 286 -288 0
436 -440 364 0
444 -236 276 0
-64 146 272 0
-49 -64 -265 0
-120 187 274 0
206 -313 -338 0
-219 250 344 0
-402 -263 433 0
207 -25 62 0
-27 127 315 0
31 320 -13 0
197 -282 315 0
136 246 163 0
-116 -440 -449 0
-413 -312 116 0
438 300 329 0
-37 -303 -93 0
-186 388 441 0
-246 129 -259 0
135 106 81 0
-449 -224 -126 0
-70 -122 -202 0
-408 -187 337 0
-351 -151 279 0
1 190 -168 0
446 175 -60 0
-79 413 28 0
353 -184 -238 0
81 370 -248 0
340 233 94 0
418 318 -433 0
397 -415 -260 0
-269 92 78 0
415 406 27 0
-206 -116 131 0
131 197 188 0
265 -245 -372 0
207 254 209 0
406 62 184 0
430 -239 266 0
-304 -366 141 0
-5 -429 213 0
159 320 22 0
449 62 -370 0
-192 -50 329 0
406 -15 431 0
358 -253 66 0
-226 259 -132 0
104 437 300 0
-12 157 167 0
9 -267 -341 0
-299 28 -288 0
-10 -422 167 0
52 78 19 0
438 -164 -168 0
256 36 397 0
351 -35 415 0
450 279 143 0
204 -445 -164 0
-125 251 -169 0
442 441 336 0
397 116 386 0
-328 -206 -402 0
-169 77 -422 0
-341 302 -445 0
-237 174 -198 0
253 -268 -413 0
-275 155 -134 0
375 137 189 0
-418 -267 -352 0
305 51 72 0
21 -4 -168 0
164 183 295 0
99 -361 -158 0
-215 50 -355 0
-224 -334 -163 0
-339 -419 178 0
425 -55 -366 0
-199 -156 376 0
-99 187 -324 0
373 435 -41 0
-158 -241 384 0
369 21 257 0
-378 -442 279 0
-378 -439 -142 0
-135 197 77 0
-340 -313 -220 0
292 105 252 0
28 424 -364 0
-268 -179 -188 0
-113 -386 110 0
394 -98 -306 0
-207 -184 228 0
-295 -106 -99 0
-187 338 -138 0
258 143 172 0
-414 -239 -175 0
-383 450 -134 0
170 327 -426 0
-356 99 153 0
-382 3 180 0
-441 274 266 0
-288 277 -430 0
152 201 -181 0
-34 -36 -449 0
47 220 -389 0
-315 361 -386 0
337 71 -306 0
-412 241 -191 0
261 -152 -164 0
-238 -148 237 0
41 234 -277 0
296 433 210 0
72 38 -95 0
306 -178 162 0
263 -375 -10 0
278 -341 -139 0
-225 -194 310 0
375 42 312 0
2 -202 -354 0
-155 -233 403 0
366 -12 92 0
-157 -448 133 0
170 -358 363 0
213 334 -317 0
237 -365 376 0
-8 57 -15 0
-138 -169 27 0
292 -101 -172 0
-211 122 148 0
214 72 103 0
-265 -219 -306 0
-219 309 302 0
-400 142 -57 0
355 438 -248 0
54 313 -421 0
-82 283 73 0
90 292 88 0
-27 348 -186 0
-103 445 -404 0
348 293 238 0
-312 126 -160 0
-275 228 -65 0
6 405 18 0
-62 331 266 0
123 -7 424 0
-133 -77 -364 0
-149 -409 218 0
-188 -148 357 0
-404 -363 66 0
-332 -345 -140 0
-249 43 -52 0
32 -328 222 0
388 -157 101 0
-274 169 -83 0
197 244 -410 0
278 -215 -313 0
248 -187 178 0
185 35 -6 0
-298 -185 -181 0
-223 317 -235 0
41 -226 -25 0
-58 -450 -351 0
364 225 -60 0
-87 159 -269 0
177 439 -282 0
-174 -370 -418 0
29 215 -345 0
-39 -122 231 0
-141 376 -50 0
-354 -228 272 0
57 180 168 0
-368 238 -302 0
-149 -304 -399 0
403 -7 346 0
301 -434 218 0
256 383 97 0
82 -381 37 0
-173 -374 -392 0
-293 -434 -114 0
89 277 -422 0
379 -42 -426 0
-155 -127 313 0
-189 159 33 0
202 -305 2 0
-309 420 190 0
-446 76 130 0
-244 -351 380 0
-376 362 423 0
-161 380 -322 0
-17 -284 187 0
-71 -108 1 0
-249 449 448 0
387 -447 426 0
-166 -390 -172 0
303 -56 308 0
56 -140 -161 0
-417 -312 367 0
148 -339 -313 0
-227 168 -270 0
205 108 -151 0
296 423 328 0
313 -348 -423 0
365 30 49 0
-392 282 292 0
296 81 -198 0
-43 159 -141 0
-299 235 -79 0
139 10 218 0
169 154 -51 0
-46 -363 415 0
102 430 -417 0
294 -375 -257 0
241 336 113 0
270 177 219 0
-266 379 -161 0
297 68 -383 0
211 315 -162 0
-126 268 -346 0
-15 -288 337 0
-132 -208 279 0
177 -197 -232 0
139 207 -281 0
-419 220 289 0
149 212 345 0
-71 346 419 0
-37 -244 176 0
-204 -152 -303 0
159 -170 -443 0
-141 114 448 0
-121 155 -95 0
49 -318 372 0
162 -277 355 0
-100 -142 -283 0
-359 -329 -11 0
191 69 211 0
-17 -156 -295 0
-351 144 402 0
-70 -188 -275 0
-26 -200 -356 0
-254 271 311 0
-294 417 263 0
-313 252 -7 0
98 -10 443 0
-171 -274 348 0
376 -275 -362 0
-288 21 335 0
449 270 318 0
252 -420 15 0
-133 153 125 0
-128 -316 -59 0
98 -325 49 0
-307 161 292 0
-400 -120 -153 0
58 166 233 0
365 185 440 0
-47 -325 397 0
330 -214 359 0
-103 -108 -323 0
149 -110 407 0
445 202 278 0
-7 -435 58 0
-289 424 -112 0
366 224 -342 0
442 -156 384 0
68 117 365 0
-275 119 383 0
-36 340 312 0
443 10 50 0
-195 137 -185 0
-269 424 -268 0
-93 -390 -288 0
7 -284 167 0
118 -280 -26 0
101 14 81 0
267 427 -388 0
406 -287 375 0
104 292 -72 0
155 -422 444 0
-371 62 -162 0
445 -447 175 0
385 339 -64 0
-351 -60 -50 0
290 -301 -328 0
193 414 223 0
-199 164 338 0
401 -75 -449 0
318 -65 -130 0
68 227 316 0
-326 -60 70 0
418 67 203 0
237 -447 -356 0
-17 199 205 0
-256 83 -431 0
243 415 65 0
203 161 -186 0
368 211 362 0
172 -17 147 0
-31 -206 -383 0
-7 165 259 0
104 -385 331 0
-172 373 185 0
-347 278 -201 0
-111 304 397 0
366 -448 198 0
260 282 -100 0
-139 -54 238 0
-447 -124 392 0
158 258 -208 0
-282 -413 387 0
315 -427 -343 0
58 376 -8 0
-289 198 305 0
150 -126 261 0
-77 204 -281 0
-311 -58 425 0
418 283 209 0
151 267 -15 0
-42 441 -133 0
-296 403 -164 0
294 375 370 0
-393 177 48 0
-365 -378 -155 0
-160 -406 193 0
-238 249 -432 0
-85 -315 -162 0
251 24 401 0
203 -104 -98 0
-249 -310 149 0
27 51 -114 0
410 -439 -162 0
81 -61 -130 0
-343 110 14 0
92 -294 -246 0
-403 -216 5 0
-279 177 -284 0
-395 -368 -207 0
379 198 388 0
1 -199 -309 0
87 202 -251 0
238 73 90 0
5 -261 -339 0
-247 308 -376 0
-387 -162 251 0
-202 -267 -373 0
-430 73 85 0
-127 -439 -76 0
-81 97 -419 0
151 346 -298 0
-411 -312 246 0
291 120 448 0
-241 425 369 0
310 -334 -340 0
29 -227 -425 0
-232 290 420 0
380 -81 -115 0
83 278 -303 0
-287 -202 -263 0
114 34 -44 0
-361 -378 287 0
-131 -86 -328 0
155 355 74 0
417 259 -220 0
249 393 391 0
-283 -47 41 0
296 -316 -280 0
345 154 184 0
141 158 -152 0
-227 92 -258 0
-96 197 251 0
-133 429 -299 0
-255 441 -153 0
301 249 -126 0
202 -62 -427 0
108 -37 433 0
84 183 -244 0
299 148 -67 0
-431 -366 357 0
96 411 221 0
-208 429 -30 0
-62 -187 136 0
309 -232 147 0
-195 44 -346 0
-401 -264 31 0
-135 -375 -232 0
-348 278 235 0
-341 -332 199 0
-313 438 155 0
-362 310 314 0
366 -11 177 0
-248 216 -10 0
-53 -309 -370 0
-273 -393 403 0
-91 -69 286 0
-11 -442 -382 0
230 440 293 0
-254 -195 -30 0
-197 146 -395 0
-438 -407 -10 0
-240 446 102 0
-155 141 -303 0
-286 -418 47 0
248 -215 164 0
11 307 -149 0
83 -151 -212 0
-381 267 -348 0
87 234 78 0
-115 -286 -109 0
354 319 177 0
93 374 16 0
-201 381 -443 0
166 -123 -227 0
-49 102 -231 0
-292 -307 -21 0
296 49 5 0
-354 -192 -60 0
173 -180 355 0
373 -359 -154 0
-426 442 400 0
-57 290 199 0
-185 369 -281 0
-229 285 123 0
294 43 -331 0
-411 104 221 0
206 89 -332 0
-84 -214 163 0
-249 192 -113 0
70 395 -162 0
-335 15 178 0
317 -330 -145 0
395 -30 278 0
-404 -184 335 0
-19 59 -163 0
314 408 -325 0
-1 -372 59 0
-142 76 15 0
-81 198 -264 0
-381 -146 315 0
190 410 -230 0
-203 208 184 0
162 -449 -134 0
-118 68 -243 0
-318 123 141 0
242 -211 -251 0
426 224 -420 0
-26 415 105 0
-334 277 319 0
325 274 89 0
-230 214 -373 0
-202 437 -116 0
155 326 -416 0
-385 347 444 0
-201 -183 -58 0
253 -278 422 0
239 196 -389 0
241 277 -396 0
7 -275 134 0
21 -206 -130 0
80 -379 364 0
106 153 -156 0
-380 7 -16 0
11 -417 -48 0
-394 10 248 0
-126 -105 -361 0
135 -319 -78 0
270 -70 422 0
232 -261 263 0
-204 -104 -361 0
-145 223 299 0
202 -15 299 0
195 364 365 0
18 386 268 0
215 -397 -346 0
-185 327 72 0
-158 372 44 0
-40 225 -54 0
406 -333 -91 0
88 59 20 0
-24 12 265 0
-78 48 -49 0
161 -276 78 0
178 -159 240 0
-75 -343 -233 0
86 -353 -34 0
436 -339 -40 0
136 339 384 0
-152 -4 -184 0
-387 218 -158 0
39 95 434 0
-50 353 267 0
-443 317 296 0
359 -69 -174 0
-142 409 261 0
28 -53 -194 0
390 13 193 0
-193 -22 -373 0
25 288 231 0
-331 99 -391 0
79 -118 -178 0
367 -144 54 0
-44 -248 -133 0
-379 -445 -319 0
-136 -56 -119 0
-69 -135 308 0
7 344 369 0
-98 -122 -131 0
-133 -445 -429 0
-148 20 32 0
-42 195 -260 0
434 -321 -327 0
292 -411 259 0
245 -422 -273 0
-316 -408 174 0
220 190 -309 0
76 21 -236 0
-124 322 -90 0
135 -270 -38 0
-303 -360 57 0
380 -448 332 0
-399 45 387 0
150 149 219 0
-360 71 -404 0
-23 -387 -284 0
169 10 396 0
-364 -102 -5 0
-302 -103 409 0
106 417 -370 0
-255 -372 71 0
-55 111 -300 0
-436 -167 -420 0
-311 -287 -245 0
426 41 -215 0
438 -245 20 0
338 -81 -95 0
-309 114 -195 0
-172 -430 412 0
-443 -293 87 0
-84 -334 2 0
341 181 197 0
-199 -59 66 0
139 62 66 0
-68 -30 268 0
-271 -149 158 0
-243 -368 405 0
-314 26 -129 0
-399 -190 185 0
-291 299 -444 0
29 110 304 0
122 -198 -87 0
179 -163 252 0
-260 201 423 0
58 357 -10 0
-165 376 34 0
377 -231 -438 0
217 289 119 0
86 -353 -276 0
87 251 -129 0
-132 418 -62 0
-146 -177 402 0
214 376 412 0
-165 110 147 0
394 58 -266 0
-27 253 -254 0
144 430 -22 0
190 -112 -103 0
56 -227 -277 0
386 434 206 0
-145 -215 335 0
-83 -120 259 0
283 248 -292 0
-248 276 209 0
-144 -216 28 0
-239 -285 -280 0
-208 397 -103 0
-21 209 333 0
-194 -412 264 0
378 73 -129 0
-419 22 -50 0
103 267 -241 0
232 121 -114 0
174 52 414 0
102 -450 -229 0
288 -87 332 0
271 -183 126 0
-136 170 -302 0
379 155 -141 0
354 -90 -99 0
-293 -121 88 0
-395 9 -348 0
121 20 390 0
-102 -232 -186 0
-348 347 -94 0
-253 238 26 0
-116 -334 -92 0
408 37 276 0
-137 -186 192 0
313 -98 338 0
-396 -257 -260 0
113 -151 201 0
193 -211 266 0
52 158 260 0
-363 -401 59 0
228 80 89 0
202 193 -402 0
-265 -297 -374 0
-34 -220 -405 0
415 313 314 0
194 -412 -134 0
-426 -190 -302 0
-180 78 335 0
-328 77 -362 0
424 -100 -263 0
106 429 261 0
-90 -184 -104 0
-372 153 -251 0
192 332 -391 0
267 264 15 0
115 356 -429 0
199 -235 -243 0
-75 428 -114 0
290 229 319 0
297 36 -235 0
-371 224 -29 0
140 -373 176 0
101 402 -40 0
-117 70 172 0
154 -361 144 0
348 51 -286 0
265 -408 341 0
204 217 190 0
-26 -276 277 0
-348 316 93 0
-190 -272 214 0
-163 385 -295 0
-346 205 394 0
22 251 4 0
337 -71 1 0
40 -198 81 0
177 366 285 0
313 445 -109 0
-242 327 -76 0
195 285 212 0
327 434 378 0
-170 -51 -209 0
365 -285 276 0
192 -388 407 0
-186 91 -50 0
215 414 60 0
-216 -359 -64 0
374 73 27 0
131 -415 325 0
-70 317 372 0
-322 -84 -428 0
-127 162 129 0
450 233 -61 0
-112 -47 190 0
-288 -367 -277 0
321 -53 218 0
-305 438 228 0
253 -411 -113 0
86 -199 224 0
227 138 -433 0
90 230 123 0
-125 371 280 0
172 -383 -18 0
446 235 -411 0
-256 288 232 0
139 205 279 0
56 -182 440 0
-190 -428 141 0
-349 137 -87 0
-90 -241 166 0
-136 207 -256 0
222 277 -262 0
162 -417 -366 0
-421 245 390 0
-196 267 440 0
-136 -239 344 0
216 307 242 0
441 -362 427 0
163 -199 332 0
110 -72 -378 0
-258 219 -247 0
20 -391 -149 0
-116 320 311 0
-371 103 -449 0
256 -396 417 0
-45 -39 344 0
238 23 -446 0
-253 20 242 0
-176 -258 -318 0
227 -202 -384 0
166 450 -290 0
-307 -433 -373 0
-106 76 -196 0
-180 -281 -259 0
301 -22 99 0
401 -444 -370 0
115 345 73 0
-260 423 -158 0
-443 39 397 0
78 -252 -104 0
380 96 28 0
265 52 44 0
127 153 146 0
-211 -84 159 0
64 192 -432 0
-310 -204 388 0
205 234 334 0
-135 323 266 0
-242 -431 -251 0
425 -324 -229 0
115 -42 -165 0
446 409 24 0
269 -26 447 0
225 -60 245 0
446 115 -264 0
188 30 137 0
-162 94 -153 0
-226 354 -264 0
125 310 -447 0
216 201 -179 0
-432 -405 329 0
43 -291 -319 0
-87 -99 -117 0
202 -283 356 0
-426 -60 379 0
360 78 -213 0
-49 -273 229 0
-244 -163 -169 0
86 43 -80 0
-298 413 -181 0
102 -394 -261 0
-12 231 39 0
291 -261 340 0
-187 33 -397 0
140 -23 -273 0
-119 163 290 0
-395 -400 -345 0
-269 -282 -185 0
184 -68 392 0
-4 209 -187 0
-276 -279 -395 0
-3 202 -21 0
-359 37 -87 0
-263 163 -372 0
-154 -411 103 0
222 447 -83 0
389 -150 -400 0
-80 -412 291 0
358 411 354 0
45 -351 90 0
-175 -416 -390 0
-114 -210 -22 0
402 -365 386 0
3 -362 -396 0
-24 344 -297 0
-280 -251 -205 0
-165 -89 156 0
-196 244 -78 0
-191 193 -400 0
-160 354 -355 0
416 333 440 0
-78 217 358 0
-232 171 79 0
273 -92 271 0
-75 45 66 0
26 -444 -300 0
1 15 83 0
365 228 -76 0
-156 -154 360 0
200 -300 109 0
-34 64 424 0
-376 211 -217 0
-174 358 187 0
-16 360 -193 0
13 54 312 0
105 448 -170 0
132 214 -150 0
290 -317 -362 0
273 -84 281 0
436 -349 221 0
-147 -99 281 0
-114 21 224 0
-238 183 -274 0
-401 -34 156 0
368 403 -154 0
344 -427 -254 0
219 -301 -121 0
-180 -417 -13 0
425 345 -92 0
7 348 -393 0
-162 -242 40 0
258 219 -62 0
-404 269 -436 0
338 -241 -232 0
347 -422 -362 0
371 -399 -212 0
-62 414 -311 0
115 -60 280 0
212 446 -142 0
-200 265 257 0
412 -185 -36 0
-303 -40 103 0
-221 399 434 0
275 -58 -151 0
298 -239 -136 0
-304 394 -180 0
-6 282 94 0
389 -285 123 0
-97 -301 40 0
449 -38 -159 0
-113 420 -190 0
146 152 260 0
135 13 291 0
-140 -173 145 0
169 -121 129 0
-275 -213 -296 0
132 -52 -183 0
-125 417 -282 0
-27 11 -167 0
-386 350 -347 0
409 -362 -105 0
-215 -90 -238 0
235 -92 -291 0
262 -145 186 0
-185 -98 -153 0
215 132 -25 0
41 -71 -292 0
-163 -251 176 0
-303 -207 46 0
387 -63 -238 0
163 -447 386 0
28 -285 407 0
256 81 -290 0
-390 -426 369 0
415 44 30 0
222 -26 -426 0
-442 -96 -268 0
-93 -420 86 0
210 120 87 0
385 92 275 0
188 256 16 0
-339 387 -420 0
-82 76 -259 0
-366 195 -282 0
347 263 -150 0
-133 91 -308 0
371 -214 -338 0
-78 -238 439 0
214 367 -365 0
-279 162 -153 0
-201 277 -41 0
-115 11 -205 0
352 -422 56 0
143 -28 393 0
-154 137 -27 0
239 -422 -250 0
-39 -25 -81 0
204 105 111 0
-120 33 -242 0
-64 39 -207 0
-323 269 -46 0
150 386 155 0
-285 -235 -445 0
-242 339 -135 0
10 430 257 0
-409 -186 22 0
-317 339 82 0
371 -384 -275 0
-418 282 28 0
39 -403 363 0
-74 412 326 0
-77 150 -327 0
319 -12 -153 0
-415 248 -97 0
-272 -250 391 0
-81 -300 439 0
-448 -228 16 0
-360 116 -55 0
75 265 43 0
-358 -443 112 0
4 315 198 0
404 165 179 0
25 -107 -325 0
12 172 344 0
-274 -276 193 0
-154 -104 -62 0
-166 -365 -345 0
321 431 230 0
-416 287 -366 0
7 349 -104 0
-428 90 254 0
-433 -340 6 0
-167 22 388 0
75 -17 60 0
-142 5 -223 0
-197 -281 -437 0
-441 -156 -425 0
133 -25 193 0
447 -317 308 0
-399 -369 450 0
-323 339 374 0
141 -71 -123 0
270 433 -346 0
-237 439 -337 0
105 76 -90 0
442 -36 -64 0
-377 431 -389 0
302 388 -73 0
383 298 -275 0
-20 -334 427 0
-86 154 -192 0
95 -104 -145 0
316 76 -25 0
-103 -261 303 0
-351 26 398 0
208 90 -216 0
-175 -52 102 0
340 405 -182 0
-27 -42 -73 0
-74 -267 289 0
200 -276 149 0
-330 -214 -211 0
310 425 212 0
417 324 -133 0
353 -295 204 0
339 -359 87 0
349 312 411 0
-383 299 -217 0
-81 -33 -102 0
431 119 229 0
-399 150 -449 0
-196 -179 131 0
-185 336 -367 0
306 -123 444 0
442 -299 -259 0
428 338 261 0
-366 -216 -42 0
-31 -362 440 0
-115 -51 174 0
-75 -136 97 0
344 -8 120 0
207 95 203 0
319 -251 52 0
390 -120 127 0
-210 -427 126 0
200 220 -443 0
51 261 313 0
171 -307 -166 0
129 -156 161 0
-363 -158 -166 0
-195 -65 42 0
-116 90 -263 0
372 110 50 0
174 -238 142 0
-432 -113 -277 0
328 79 -341 0
-270 -331 54 0
-48 184 165 0
-103 221 -112 0
-13 -369 -30 0
-387 310 -367 0
-293 78 211 0
97 -164 -63 0
202 388 299 0
302 279 -426 0
-142 44 -409 0
94 19 -160 0
-90 -91 290 0
-205 152 106 0
59 -339 341 0
-230 -450 385 0
418 -50 -53 0
-431 -184 445 0
417 329 -221 0
-101 -32 205 0
20 216 -218 0
15 306 -152 0
-334 123 153 0
-210 92 -102 0
-361 -177 -22 0
315 -152 285 0
375 321 129 0
78 -225 242 0
-325 -390 209 0
-317 83 38 0
249 142 312 0
-330 -430 -405 0
-420 301 -197 0
405 330 263 0
52 -308 412 0
230 -375 -447 0
82 -105 107 0
-129 -142 -22 0
210 32 97 0
154 329 204 0
-371 52 -76 0
-185 298 446 0
-206 89 181 0
-131 119 16 0
435 -231 -357 0
412 -415 88 0
257 272 43 0
-340 290 -389 0
236 -138 10 0
-235 23 -210 0
291 140 17 0
412 141 -446 0
432 -402 -157 0
225 55 -359 0
181 210 -221 0
7 -60 386 0
-145 44 -3 0
179 202 249 0
210 77 -404 0
358 -36 427 0
-97 -44 -88 0
-296 395 80 0
-289 406 131 0
-221 -105 24 0
286 -306 109 0
-243 -435 -98 0
-226 36 -67 0
64 437 -61 0
317 228 439 0
417 -134 -253 0
-173 -338 104 0
-237 -94 99 0
-157 372 63 0
-65 20 379 0
295 -404 408 0
245 -185 312 0
-446 182 -126 0
-115 213 -255 0
-38 -19 92 0
27 -231 25 0
350 -201 290 0
-214 -67 -90 0
-274 -379 -241 0
74 77 -183 0
221 -203 283 0
42 197 -276 0
-412 291 -446 0
61 89 219 0
110 -394 -409 0
293 57 172 0
381 430 -377 0
95 144 125 0
160 -315 -417 0
-286 -437 -334 0
331 -446 -410 0
-295 70 315 0
-178 40 119 0
220 -412 -396 0
-323 52 -302 0
-136 430 -429 0
383 -110 -32 0
16 -184 199 0
343 66 195 0
-356 110 449 0
381 -439 -61 0
390 -9 -216 0
-70 -319 -327 0
-24 222 26 0
-233 -422 185 0
347 -338 189 0
-393 -443 198 0
342 312 -158 0
-32 222 -39 0
-319 134 215 0
342 -67 137 0
361 231 289 0
154 -203 -316 0
171 265 -353 0
-332 271 317 0
-182 -234 48 0
-318 -395 -186 0
188 332 -214 0
-346 -340 424 0
293 413 -394 0
-74 -253 426 0
-72 -62 -34 0
277 -91 134 0
-445 265 -318 0
31 392 -256 0
61 -198 -364 0
-54 -352 30 0
-412 98 -114 0
124 133 -4 0
436 440 -326 0
329 -433 136 0
445 -244 -419 0
-5 -109 -401 0
127 166 293 0
39 388 358 0
166 -265 9 0
-323 -191 -312 0
-324 -54 -230 0
317 393 -293 0
-243 281 -48 0
145 164 -225 0
375 -140 -320 0
145 -331 -7 0
400 213 339 0
93 383 54 0
-243 118 -39 0
-132 5 -389 0
-208 216 -46 0
70 77 274 0
-47 -93 302 0
-74 356 446 0
-405 376 346 0
401 315 214 0
250 227 -411 0
143 -360 422 0
396 -151 3 0
164 239 167 0
177 -257 66 0
-244 82 358 0
-19 213 -227 0
100 201 -26 0
373 -237 -46 0
427 337 -363 0
-357 -76 -156 0
-312 297 -115 0
-263 265 111 0
325 -138 45 0
-303 214 -27 0
133 -32 -128 0
-30 60 164 0
-165 370 34 0
88 -395 -109 0
-36 411 -344 0
-85 271 26 0
68 -96 404 0
-208 414 68 0
23 7 -442 0
56 -260 -271 0
-310 -276 -388 0
67 -172 -293 0
122 -389 -449 0
195 -159 -33 0
200 -370 -417 0
-270 21 348 0
108 331 -308 0
-25 -243 95 0
-360 46 -242 0
-389 -360 -100 0
139 325 184 0
443 58 32 0
-115 -379 126 0
-173 139 213 0
97 -402 116 0
245 72 17 0
-431 -349 123 0
70 266 237 0
-219 330 305 0
427 110 -257 0
175 163 -292 0
395 -298 261 0
10 110 -191 0
288 -123 -65 0
-373 -189 -174 0
71 -52 -12 0
-347 -356 -438 0
364 250 -51 0
27 386 -188 0
336 301 -3 0
-294 55 -122 0
-305 -390 290 0
55 327 301 0
-262 253 -356 0
312 298 -341 0
-248 -371 186 0
243 254 -282 0
-413 310 141 0
-413 -344 311 0
-233 368 -68 0
-443 60 381 0
32 249 180 0
-219 -11 234 0
-278 219 182 0
62 -321 284 0
-7 61 401 0
-143 423 427 0
-109 296 -89 0
351 232 280 0
-426 15 -267 0
81 -51 363 0
80 343 -105 0
-70 25 -144 0
-171 277 -418 0
60 215 -160 0
368 240 -92 0
-246 248 -100 0
331 -347 16 0
-137 352 304 0
355 -67 -256 0
360 -390 106 0
436 143 -226 0
-446 -300 -44 0
-172 -355 298 0
131 -341 -441 0
110 22 -271 0
203 262 -329 0
-319 331 -130 0
-203 -237 77 0
-250 48 -101 0
217 -196 -37 0
-61 390 58 0
91 -296 -399 0
-256 78 148 0
-48 226 -258 0
105 -78 247 0
-189 -349 422 0
59 88 -204 0
-413 386 31 0
246 218 239 0
445 26 156 0
75 284 -298 0
435 -233 166 0
-432 -30 31 0
385 -274 89 0
-164 -343 425 0
56 -337 -4 0
-199 -151 439 0
319 207 -204 0
24 280 406 0
-179 -130 -321 0
-106 -378 -128 0
-55 -103 -396 0
359 -109 -132 0
-375 75 -234 0
-349 230 427 0
-284 -173 -70 0
263 205 -323 0
-83 -186 -428 0
223 125 11 0
420 -313 211 0
-432 327 58 0
-404 243 65 0
-198 214 325 0
447 98 -87 0
-7 -152 -178 0
176 355 -138 0
-11 -371 -151 0
-317 -39 -130 0
-65 23 260 0
289 -330 -201 0
372 -57 -139 0
-127 -6 -192 0
-85 -110 293 0
382 216 3 0
239 -292 -407 0
-46 -217 -379 0
324 257 -105 0
431 -200 169 0
7 -70 -267 0
84 176 -229 0
-319 81 32 0
-355 -191 44 0
383 -298 -81 0
-403 123 24 0
115 -186 -315 0
-104 78 32 0
154 242 159 0
36 397 386 0
-24 131 9 0
360 -125 203 0
113 160 -200 0
234 -414 -313 0
369 204 134 0
-341 249 307 0
65 115 328 0
-137 -128 -295 0
-444 411 291 0
419 -97 113 0
141 -117 344 0
-58 -4 147 0
148 217 -194 0
368 312 -349 0
117 351 119 0
136 -82 -130 0
51 201 -237 0
163 -287 273 0
-354 -215 49 0
41 446 -441 0
-408 57 427 0
-240 221 -324 0
-289 -418 361 0
195 93 -65 0
-246 166 -258 0
-423 -178 -256 0
-357 -190 181 0
-304 120 11 0
-366 -312 19 0
281 200 -22 0
54 104 369 0
-309 -43 168 0
-294 253 221 0
-64 -263 -119 0
-432 -97 -65 0
-199 -397 -272 0
54 -247 -368 0
209 -210 413 0
437 293 409 0
185 248 255 0
-268 328 -215 0
438 -9 -122 0
34 447 367 0
222 -376 165 0
416 -418 248 0
215 -192 -226 0
237 54 -302 0
-266 55 -220 0
201 257 -245 0
-95 71 -325 0
-332 392 188 0
156 -72 242 0
-51 -377 -287 0
-273 55 267 0
175 -337 -106 0
-383 35 366 0
370 247 -44 0
-273 -239 384 0
85 -313 -177 0
-163 133 -98 0
121 -320 -189 0
87 -367 265 0
-270 426 -35 0
185 -153 18 0
355 45 358 0
-173 359 372 0
-198 398 174 0
11 -203 115 0
-12 -411 -195 0
-257 165 332 0
447 287 341 0
296 -358 -269 0
209 169 422 0
-287 365 325 0
210 422 -266 0
-281 172 -23 0
380 91 42 0
267 310 -114 0
-417 -306 -376 0
380 -65 -292 0
-1 413 -378 0
9 219 -448 0
71 -378 377 0
-329 -276 202 0
-246 -141 -198 0
109 145 -247 0
-276 15 150 0
-288 132 -80 0
-26 369 -277 0
-21 -155 13 0
71 311 -433 0
-379 412 25 0
240 -155 -220 0
-290 -91 -418 0
-422 36 -388 0
274 147 -393 0
-186 -378 -12 0
359 192 -163 0
-63 -378 424 0
-217 -439 -413 0
-317 -277 -320 0
231 -398 -121 0
-429 160 -9 0
39 -90 -299 0
-435 234 -191 0
276 245 117 0
-5 43 72 0
307 87 -6 0
-244 376 -312 0
-282 77 8 0
96 46 3 0
149 -333 4 0
375 -326 -154 0
-129 -172 -7 0
-172 -194 -188 0
-249 20 396 0
425 349 -318 0
202 -79 -66 0
-95 -376 -407 0
388 348 387 0
-421 23 197 0
-279 358 -243 0
305 27 -410 0
-136 -78 194 0
85 -5 179 0
-332 297 -64 0
-143 356 198 0
-196 -20 -187 0
-145 135 -350 0
-69 -296 393 0
196 94 -404 0
264 -298 430 0
-391 406 150 0
-136 405 404 0
10 377 363 0
-443 419 -329 0
425 223 -295 0
-51 -214 252 0
-359 -148 98 0
276 21 -387 0
-277 142 -151 0
201 281 -267 0
-375 50 -211 0
256 -298 -343 0
-104 -164 -174 0
280 -371 -267 0
-182 68 346 0
119 251 -316 0
-122 -57 -113 0
423 176 38 0
-129 390 -270 0
422 -284 -393 0
-399 -36 -408 0
-157 437 -232 0
185 -81 397 0
-10 -352 -431 0
-286 369 410 0
280 -122 -178 0
182 445 394 0
-372 -95 85 0
378 -410 -95 0
81 -299 -248 0
444 89 374 0
374 338 167 0
445 440 -344 0
387 -390 -430 0
260 -221 -95 0
-6 357 47 0
-52 -44 -230 0
196 175 -450 0
-445 -34 -270 0
-240 -173 186 0
-383 10 -80 0
-75 -177 -412 0
-139 -439 -330 0
266 -14 398 0
-240 -242 -236 0
-264 97 272 0
250 308 44 0
280 411 29 0
-237 440 -182 0
298 213 -118 0
44 -75 320 0
-154 58 185 0
-423 -13 -332 0
375 312 -106 0
55 259 86 0
-384 295 195 0
148 280 -71 0
280 337 80 0
307 -200 286 0
-239 364 187 0
341 -160 385 0
323 101 168 0
-399 -177 141 0
43 81 175 0
400 -198 -444 0
-91 349 217 0
-303 -388 446 0
75 238 -33 0
314 392 61 0
-226 66 14 0
-380 270 68 0
52 -29 -368 0
113 -244 158 0
-325 -3 -196 0
25 -227 -45 0
52 161 137 0
48 298 433 0
-438 -412 362 0
326 -188 435 0
305 179 237 0
183 -426 275 0
220 382 360 0
-132 189 287 0
-433 57 -370 0
50 15 -115 0
151 161 146 0
-380 -97 -162 0
181 208 -15 0
-55 334 324 0
46 -150 -246 0
260 142 159 0
-43 125 -358 0
-114 423 -44 0
-446 354 370 0
-319 -431 -335 0
-309 69 -379 0
333 -243 -394 0
-450 205 -437 0
-347 152 -248 0
72 -142 -38 0
450 234 15 0
412 -448 292 0
-257 253 147 0
73 86 400 0
30 434 193 0
-322 -437 -69 0
-213 265 -425 0
-270 79 -28 0
185 -107 31 0
-168 374 -113 0
-293 295 -281 0
3 283 -17 0
-96 328 376 0
344 442 152 0
-59 -17 18 0
-279 341 330 0
-22 -177 339 0
-141 116 244 0
-307 449 23 0
-196 301 -198 0
-353 52 -334 0
-416 -317 378 0
340 -80 176 0
250 279 419 0
383 -76 -95 0
-441 26 302 0
-196 142 -85 0
-413 -192 41 0
-362 -5 183 0
107 -279 -31 0
-10 -52 145 0
-348 308 233 0
304 -257 -394 0
401 -7 214 0
16 -163 444 0
132 149 -309 0
-269 -151 324 0
405 387 -74 0
-192 -224 -328 0
427 194 -82 0
-209 -393 -62 0
414 72 -232 0
-110 -222 415 0
-96 -276 280 0
-71 422 412 0
242 6 228 0
402 -335 -267 0
251 373 -406 0
-91 -19 216 0
91 444 -43 0
-414 -309 370 0
-264 -299 291 0
83 404 51 0
291 23 317 0
-104 -277 32 0
213 12 -435 0
-177 44 -433 0
-181 -200 176 0
-110 9 5 0
423 -277 401 0
407 137 265 0
270 -350 282 0
-60 16 -347 0
-308 131 -446 0
-292 -327 98 0
367 376 219 0
-183 -57 -412 0
383 -5 259 0
-302 -132 -334 0
-162 -188 68 0
313 102 288 0
-201 435 303 0
87 -363 -186 0
-135 334 249 0
-316 -107 -297 0
217 -402 144 0
147 -410 324 0
329 388 187 0
82 350 237 0
-206 215 328 0
187 -148 -347 0
258 285 381 0
228 358 -60 0
170 -154 -224 0
133 -153 -58 0
-357 -425 -65 0
-73 -48 173 0
-3 301 304 0
205 73 180 0
-176 -129 249 0
-297 96 -113 0
-169 376 370 0
200 -296 263 0
-108 -442 -79 0
335 -146 -204 0
-158 64 -153 0
-307 435 -48 0
-73 111 -17 0
387 46 -105 0
-232 -402 87 0
361 -209 162 0
21 267 -235 0
257 -323 18 0
341 -3 164 0
372 136 -276 0
-66 -96 58 0
435 200 399 0
-450 -131 352 0
23 -384 -181 0
-365 -55 -301 0
68 301 -166 0
162 56 -182 0
-170 104 -395 0
-41 -57 280 0
-411 253 -204 0
-183 26 449 0
-417 -429 232 0
39 19 260 0
341 70 411 0
321 407 -418 0
-100 -152 305 0
-305 64 -21 0
77 396 -159 0
-320 414 369 0
-400 -86 362 0
441 -381 -223 0
238 376 104 0
-354 250 -11 0
-239 -272 -77 0
353 -448 357 0
-254 224 401 0
-129 -347 441 0
-98 299 79 0
-49 -71 351 0
-122 -396 212 0
358 415 -316 0
-204 -414 349 0
-327 200 -258 0
-152 -159 -116 0
-379 -241 -147 0
-429 -195 -163 0
277 -279 -324 0
-274 -122 95 0
-388 -165 316 0
60 -305 -421 0
-330 -45 -238 0
298 2 -231 0
62 79 317 0
53 320 -299 0
181 249 186 0
149 -445 -383 0
285 -259 68 0
310 -215 -97 0
448 -301 388 0
114 -60 36 0
81 447 -384 0
435 369 -214 0
-344 -191 -184 0
274 -341 -361 0
-304 -442 32 0
-372 68 355 0
-49 -194 295 0
-98 -156 437 0
48 139 256 0
419 -38 423 0
54 349 317 0
-36 78 396 0
66 144 -160 0
-262 81 -153 0
264 282 -156 0
133 -412 -340 0
361 -443 -378 0
-212 411 -263 0
243 64 -154 0
-412 -117 216 0
-387 327 -382 0
341 300 153 0
-210 82 -400 0
202 10 -293 0
159 47 155 0
395 184 209 0
294 29 -229 0
126 364 274 0
411 -38 440 0
-188 301 -427 0
82 -200 9 0
349 333 -381 0
344 48 418 0
443 384 420 0
-425 11 224 0
274 -260 -407 0
376 68 155 0
-101 -170 413 0
203 306 234 0
-85 29 300 0
288 -59 37 0
114 341 -4 0
-404 103 -27 0
-363 178 377 0
418 -252 141 0
312 178 302 0
352 -364 -404 0
9 -317 -82 0
224 388 29 0
182 421 -139 0
209 -308 165 0
210 198 306 0
-270 258 -377 0
-262 433 212 0
-175 -411 -299 0
290 49 370 0
-35 -238 -79 0
-376 -64 -345 0
231 409 180 0
290 -202 -410 0
30 47 425 0
-395 -122 18 0
285 -325 72 0
-143 -103 -12 0
378 -189 -244 0
80 418 280 0
403 -260 -282 0
-47 172 379 0
52 435 145 0
-331 296 359 0
-410 -342 443 0
-279 -106 327 0
-209 -390 -181 0
-367 290 -118 0
62 320 101 0
-99 -146 407 0
-238 -304 -115 0
-161 201 -410 0
187 108 -389 0
28 221 252 0
-399 217 -255 0
417 -37 67 0
418 -350 379 0
-335 -375 -7 0
-225 25 351 0
-366 -106 223 0
416 46 -428 0
216 379 -411 0
210 391 -338 0
-370 -58 342 0
-304 -135 175 0
419 216 69 0
-312 -184 110 0
69 -238 -41 0
-45 163 358 0
-247 359 -354 0
-417 412 167 0
-362 -219 141 0
-402 -232 81 0
-8 -200 -401 0
226 422 -140 0
426 -210 126 0
-85 371 207 0
262 -229 -431 0
-385 -188 125 0
232 -121 -16 0
155 -5 -445 0
-183 138 -33 0
38 75 -64 0
274 -88 -409 0
247 446 309 0
-181 338 -263 0
436 396 43 0
143 281 -139 0
104 -217 417 0
-124 14 -76 0
16 -178 144 0
333 -310 406 0
432 -199 -78 0
343 -305 -284 0
-13 172 -415 0
4 174 -116 0
-169 47 90 0
-161 -114 -404 0
-411 327 178 0
301 249 -390 0
-342 -367 -448 0
331 -145 -77 0
449 140 289 0
6 312 -283 0
269 234 -214 0
-116 366 54 0
327 60 -106 0
61 -187 59 0
128 154 438 0
-291 -368 -372 0
-160 -254 -66 0
266 -77 337 0
-199 -237 315 0
-219 301 338 0
-18 -362 -343 0
406 266 -30 0
187 -46 -396 0
-152 312 61 0
161 -235 24 0
65 67 -215 0
-60 80 -171 0
-92 440 424 0
-353 -216 -55 0
284 -306 -327 0
367 244 -307 0
-161 261 116 0
-343 -252 -153 0
-52 178 -131 0
-213 264 -431 0
290 -429 163 0
313 -36 395 0
423 381 226 0
-206 373 -314 0
325 320 306 0
-316 317 -226 0
-298 -83 384 0
6 417 194 0
280 -90 166 0
-29 -13 409 0
-432 -59 179 0
274 -187 -294 0
298 331 373 0
278 144 305 0
367 275 181 0
52 -238 178 0
206 133 94 0
-329 -37 -338 0
-224 -408 -427 0
-19 -68 436 0
-110 408 -55 0
267 372 170 0
337 32 -75 0
131 -309 -304 0
201 -199 -348 0
42 48 -163 0
283 50 52 0
13 271 -98 0